(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), x, a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
red[Let][Let](e, Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](e, App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](e, V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](App(e1, e2), f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, x, a, e) → e
subst[Ite](True, x, a, e) → a
Rewrite Strategy: INNERMOST
(1) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
subst[Ite]/1
red[Let][Let]/0
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a
Rewrite Strategy: INNERMOST
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
subst(x, a, App(e1, e2)) →+ mkapp(subst(x, a, e1), subst(x, a, e2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [e1 / App(e1, e2)].
The result substitution is [ ].
(4) BOUNDS(n^1, INF)